Nuprl Lemma : member_upto2
0,22
postcript
pdf
n
,
i
:
.
i
<
n
(
i
upto(
n
))
latex
Definitions
(
x
l
)
,
x
:
A
.
B
(
x
)
,
Prop
,
upto(
n
)
,
||
as
||
,
A
&
B
,
,
{
i
..
j
}
,
A
,
False
,
P
Q
,
l
[
i
]
,
i
j
<
k
,
P
&
Q
,
A
B
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
le
wf
,
select
upto
,
length
upto
,
select
wf
,
upto
wf
,
int
seg
wf
,
length
wf1
,
nat
wf
origin
n, i:
. i<n 
(i 
upto(n)) n, i:. i<n (i upto(n)) l)
x:A. B(x)
}
A Q
j < kBx:A. B(x) T